<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>QuickLaTeX</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

</a><a id="63" class="Markup">\begin{code}</a>
<a id="76" class="Symbol">{-#</a> <a id="80" class="Keyword">OPTIONS</a> <a id="88" class="Pragma">--sized-types</a> <a id="102" class="Symbol">#-}</a>

<a id="107" class="Symbol">{-#</a> <a id="111" class="Keyword">BUILTIN</a> <a id="119" class="Keyword">SIZE</a> <a id="Size"></a><a id="124" href="QuickLaTeX.html#124" class="Postulate">Size</a> <a id="129" class="Symbol">#-}</a>

<a id="134" class="Keyword">record</a> <a id="Sigma"></a><a id="141" href="QuickLaTeX.html#141" class="Record">Sigma</a> <a id="147" class="Symbol">(</a><a id="148" href="QuickLaTeX.html#148" class="Bound">A</a> <a id="150" class="Symbol">:</a> <a id="152" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="155" class="Symbol">)</a> <a id="157" class="Symbol">(</a><a id="158" href="QuickLaTeX.html#158" class="Bound">B</a> <a id="160" class="Symbol">:</a> <a id="162" href="QuickLaTeX.html#148" class="Bound">A</a> <a id="164" class="Symbol">→</a> <a id="166" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="169" class="Symbol">)</a> <a id="171" class="Symbol">:</a> <a id="173" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="177" class="Keyword">where</a>
  <a id="185" class="Keyword">coinductive</a>
  <a id="199" class="Keyword">constructor</a> <a id="c"></a><a id="211" href="QuickLaTeX.html#211" class="CoinductiveConstructor">c</a>
  <a id="215" class="Keyword">field</a>
    <a id="Sigma.proj₁"></a><a id="225" href="QuickLaTeX.html#225" class="Field">proj₁</a> <a id="231" class="Symbol">:</a> <a id="233" href="QuickLaTeX.html#148" class="Bound">A</a>
    <a id="Sigma.proj₂"></a><a id="239" href="QuickLaTeX.html#239" class="Field">proj₂</a> <a id="245" class="Symbol">:</a> <a id="247" href="QuickLaTeX.html#158" class="Bound">B</a> <a id="249" href="QuickLaTeX.html#225" class="Field">proj₁</a>

<a id="256" class="Keyword">data</a> <a id="D"></a><a id="261" href="QuickLaTeX.html#261" class="Datatype">D</a> <a id="263" class="Symbol">:</a> <a id="265" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="269" class="Keyword">where</a>
  <a id="D.c"></a><a id="277" href="QuickLaTeX.html#277" class="InductiveConstructor">c</a> <a id="279" class="Symbol">:</a> <a id="281" href="QuickLaTeX.html#261" class="Datatype">D</a>

<a id="f"></a><a id="284" href="QuickLaTeX.html#284" class="Function">f</a> <a id="286" class="Symbol">:</a> <a id="288" class="Symbol">{</a><a id="289" href="QuickLaTeX.html#289" class="Bound">A</a> <a id="291" class="Symbol">:</a> <a id="293" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="296" class="Symbol">}</a> <a id="298" class="Symbol">{</a><a id="299" href="QuickLaTeX.html#299" class="Bound">B</a> <a id="301" class="Symbol">:</a> <a id="303" href="QuickLaTeX.html#289" class="Bound">A</a> <a id="305" class="Symbol">→</a> <a id="307" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="310" class="Symbol">}</a> <a id="312" class="Symbol">(</a><a id="313" href="QuickLaTeX.html#313" class="Bound">x</a> <a id="315" class="Symbol">:</a> <a id="317" href="QuickLaTeX.html#289" class="Bound">A</a><a id="318" class="Symbol">)</a> <a id="320" class="Symbol">→</a> <a id="322" href="QuickLaTeX.html#299" class="Bound">B</a> <a id="324" href="QuickLaTeX.html#313" class="Bound">x</a> <a id="326" class="Symbol">→</a> <a id="328" href="QuickLaTeX.html#141" class="Record">Sigma</a> <a id="334" href="QuickLaTeX.html#289" class="Bound">A</a> <a id="336" href="QuickLaTeX.html#299" class="Bound">B</a>
<a id="338" href="QuickLaTeX.html#284" class="Function">f</a> <a id="340" class="Symbol">=</a> <a id="342" href="QuickLaTeX.html#211" class="CoinductiveConstructor">c</a>
<a id="344" class="Markup">\end{code}</a><a id="354" class="Background">

\end{document}
</a></pre></body></html>